(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
s(log(0)) → s(0)
log(s(x)) → s(log(half(s(x))))
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
half(0) → 0
half(s(0)) → 0
half(s(s(z0))) → s(half(z0))
s(log(0)) → s(0)
log(s(z0)) → s(log(half(s(z0))))
Tuples:
HALF(s(s(z0))) → c2(S(half(z0)), HALF(z0))
S(log(0)) → c3(S(0))
LOG(s(z0)) → c4(S(log(half(s(z0)))), LOG(half(s(z0))), HALF(s(z0)), S(z0))
S tuples:
HALF(s(s(z0))) → c2(S(half(z0)), HALF(z0))
S(log(0)) → c3(S(0))
LOG(s(z0)) → c4(S(log(half(s(z0)))), LOG(half(s(z0))), HALF(s(z0)), S(z0))
K tuples:none
Defined Rule Symbols:
half, s, log
Defined Pair Symbols:
HALF, S, LOG
Compound Symbols:
c2, c3, c4
(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing nodes:
S(log(0)) → c3(S(0))
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
half(0) → 0
half(s(0)) → 0
half(s(s(z0))) → s(half(z0))
s(log(0)) → s(0)
log(s(z0)) → s(log(half(s(z0))))
Tuples:
HALF(s(s(z0))) → c2(S(half(z0)), HALF(z0))
LOG(s(z0)) → c4(S(log(half(s(z0)))), LOG(half(s(z0))), HALF(s(z0)), S(z0))
S tuples:
HALF(s(s(z0))) → c2(S(half(z0)), HALF(z0))
LOG(s(z0)) → c4(S(log(half(s(z0)))), LOG(half(s(z0))), HALF(s(z0)), S(z0))
K tuples:none
Defined Rule Symbols:
half, s, log
Defined Pair Symbols:
HALF, LOG
Compound Symbols:
c2, c4
(5) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
HALF(
s(
s(
z0))) →
c2(
S(
half(
z0)),
HALF(
z0)) by
HALF(s(s(0))) → c2(S(0), HALF(0))
HALF(s(s(s(0)))) → c2(S(0), HALF(s(0)))
HALF(s(s(s(s(z0))))) → c2(S(s(half(z0))), HALF(s(s(z0))))
HALF(s(s(x0))) → c2
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
half(0) → 0
half(s(0)) → 0
half(s(s(z0))) → s(half(z0))
s(log(0)) → s(0)
log(s(z0)) → s(log(half(s(z0))))
Tuples:
LOG(s(z0)) → c4(S(log(half(s(z0)))), LOG(half(s(z0))), HALF(s(z0)), S(z0))
HALF(s(s(0))) → c2(S(0), HALF(0))
HALF(s(s(s(0)))) → c2(S(0), HALF(s(0)))
HALF(s(s(s(s(z0))))) → c2(S(s(half(z0))), HALF(s(s(z0))))
HALF(s(s(x0))) → c2
S tuples:
LOG(s(z0)) → c4(S(log(half(s(z0)))), LOG(half(s(z0))), HALF(s(z0)), S(z0))
HALF(s(s(0))) → c2(S(0), HALF(0))
HALF(s(s(s(0)))) → c2(S(0), HALF(s(0)))
HALF(s(s(s(s(z0))))) → c2(S(s(half(z0))), HALF(s(s(z0))))
HALF(s(s(x0))) → c2
K tuples:none
Defined Rule Symbols:
half, s, log
Defined Pair Symbols:
LOG, HALF
Compound Symbols:
c4, c2, c2
(7) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 3 trailing nodes:
HALF(s(s(s(0)))) → c2(S(0), HALF(s(0)))
HALF(s(s(x0))) → c2
HALF(s(s(0))) → c2(S(0), HALF(0))
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
half(0) → 0
half(s(0)) → 0
half(s(s(z0))) → s(half(z0))
s(log(0)) → s(0)
log(s(z0)) → s(log(half(s(z0))))
Tuples:
LOG(s(z0)) → c4(S(log(half(s(z0)))), LOG(half(s(z0))), HALF(s(z0)), S(z0))
HALF(s(s(s(s(z0))))) → c2(S(s(half(z0))), HALF(s(s(z0))))
S tuples:
LOG(s(z0)) → c4(S(log(half(s(z0)))), LOG(half(s(z0))), HALF(s(z0)), S(z0))
HALF(s(s(s(s(z0))))) → c2(S(s(half(z0))), HALF(s(s(z0))))
K tuples:none
Defined Rule Symbols:
half, s, log
Defined Pair Symbols:
LOG, HALF
Compound Symbols:
c4, c2
(9) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
LOG(
s(
z0)) →
c4(
S(
log(
half(
s(
z0)))),
LOG(
half(
s(
z0))),
HALF(
s(
z0)),
S(
z0)) by
LOG(s(0)) → c4(S(log(0)), LOG(half(s(0))), HALF(s(0)), S(0))
LOG(s(s(z0))) → c4(S(log(s(half(z0)))), LOG(half(s(s(z0)))), HALF(s(s(z0))), S(s(z0)))
LOG(s(x0)) → c4
(10) Obligation:
Complexity Dependency Tuples Problem
Rules:
half(0) → 0
half(s(0)) → 0
half(s(s(z0))) → s(half(z0))
s(log(0)) → s(0)
log(s(z0)) → s(log(half(s(z0))))
Tuples:
HALF(s(s(s(s(z0))))) → c2(S(s(half(z0))), HALF(s(s(z0))))
LOG(s(0)) → c4(S(log(0)), LOG(half(s(0))), HALF(s(0)), S(0))
LOG(s(s(z0))) → c4(S(log(s(half(z0)))), LOG(half(s(s(z0)))), HALF(s(s(z0))), S(s(z0)))
LOG(s(x0)) → c4
S tuples:
HALF(s(s(s(s(z0))))) → c2(S(s(half(z0))), HALF(s(s(z0))))
LOG(s(0)) → c4(S(log(0)), LOG(half(s(0))), HALF(s(0)), S(0))
LOG(s(s(z0))) → c4(S(log(s(half(z0)))), LOG(half(s(s(z0)))), HALF(s(s(z0))), S(s(z0)))
LOG(s(x0)) → c4
K tuples:none
Defined Rule Symbols:
half, s, log
Defined Pair Symbols:
HALF, LOG
Compound Symbols:
c2, c4, c4
(11) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing nodes:
LOG(s(x0)) → c4
(12) Obligation:
Complexity Dependency Tuples Problem
Rules:
half(0) → 0
half(s(0)) → 0
half(s(s(z0))) → s(half(z0))
s(log(0)) → s(0)
log(s(z0)) → s(log(half(s(z0))))
Tuples:
HALF(s(s(s(s(z0))))) → c2(S(s(half(z0))), HALF(s(s(z0))))
LOG(s(0)) → c4(S(log(0)), LOG(half(s(0))), HALF(s(0)), S(0))
LOG(s(s(z0))) → c4(S(log(s(half(z0)))), LOG(half(s(s(z0)))), HALF(s(s(z0))), S(s(z0)))
S tuples:
HALF(s(s(s(s(z0))))) → c2(S(s(half(z0))), HALF(s(s(z0))))
LOG(s(0)) → c4(S(log(0)), LOG(half(s(0))), HALF(s(0)), S(0))
LOG(s(s(z0))) → c4(S(log(s(half(z0)))), LOG(half(s(s(z0)))), HALF(s(s(z0))), S(s(z0)))
K tuples:none
Defined Rule Symbols:
half, s, log
Defined Pair Symbols:
HALF, LOG
Compound Symbols:
c2, c4
(13) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
HALF(
s(
s(
s(
s(
z0))))) →
c2(
S(
s(
half(
z0))),
HALF(
s(
s(
z0)))) by
HALF(s(s(s(s(0))))) → c2(S(s(0)), HALF(s(s(0))))
HALF(s(s(s(s(s(0)))))) → c2(S(s(0)), HALF(s(s(s(0)))))
HALF(s(s(s(s(s(s(z0))))))) → c2(S(s(s(half(z0)))), HALF(s(s(s(s(z0))))))
HALF(s(s(s(s(x0))))) → c2
(14) Obligation:
Complexity Dependency Tuples Problem
Rules:
half(0) → 0
half(s(0)) → 0
half(s(s(z0))) → s(half(z0))
s(log(0)) → s(0)
log(s(z0)) → s(log(half(s(z0))))
Tuples:
LOG(s(0)) → c4(S(log(0)), LOG(half(s(0))), HALF(s(0)), S(0))
LOG(s(s(z0))) → c4(S(log(s(half(z0)))), LOG(half(s(s(z0)))), HALF(s(s(z0))), S(s(z0)))
HALF(s(s(s(s(0))))) → c2(S(s(0)), HALF(s(s(0))))
HALF(s(s(s(s(s(0)))))) → c2(S(s(0)), HALF(s(s(s(0)))))
HALF(s(s(s(s(s(s(z0))))))) → c2(S(s(s(half(z0)))), HALF(s(s(s(s(z0))))))
HALF(s(s(s(s(x0))))) → c2
S tuples:
LOG(s(0)) → c4(S(log(0)), LOG(half(s(0))), HALF(s(0)), S(0))
LOG(s(s(z0))) → c4(S(log(s(half(z0)))), LOG(half(s(s(z0)))), HALF(s(s(z0))), S(s(z0)))
HALF(s(s(s(s(0))))) → c2(S(s(0)), HALF(s(s(0))))
HALF(s(s(s(s(s(0)))))) → c2(S(s(0)), HALF(s(s(s(0)))))
HALF(s(s(s(s(s(s(z0))))))) → c2(S(s(s(half(z0)))), HALF(s(s(s(s(z0))))))
HALF(s(s(s(s(x0))))) → c2
K tuples:none
Defined Rule Symbols:
half, s, log
Defined Pair Symbols:
LOG, HALF
Compound Symbols:
c4, c2, c2
(15) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 3 trailing nodes:
HALF(s(s(s(s(0))))) → c2(S(s(0)), HALF(s(s(0))))
HALF(s(s(s(s(x0))))) → c2
HALF(s(s(s(s(s(0)))))) → c2(S(s(0)), HALF(s(s(s(0)))))
(16) Obligation:
Complexity Dependency Tuples Problem
Rules:
half(0) → 0
half(s(0)) → 0
half(s(s(z0))) → s(half(z0))
s(log(0)) → s(0)
log(s(z0)) → s(log(half(s(z0))))
Tuples:
LOG(s(0)) → c4(S(log(0)), LOG(half(s(0))), HALF(s(0)), S(0))
LOG(s(s(z0))) → c4(S(log(s(half(z0)))), LOG(half(s(s(z0)))), HALF(s(s(z0))), S(s(z0)))
HALF(s(s(s(s(s(s(z0))))))) → c2(S(s(s(half(z0)))), HALF(s(s(s(s(z0))))))
S tuples:
LOG(s(0)) → c4(S(log(0)), LOG(half(s(0))), HALF(s(0)), S(0))
LOG(s(s(z0))) → c4(S(log(s(half(z0)))), LOG(half(s(s(z0)))), HALF(s(s(z0))), S(s(z0)))
HALF(s(s(s(s(s(s(z0))))))) → c2(S(s(s(half(z0)))), HALF(s(s(s(s(z0))))))
K tuples:none
Defined Rule Symbols:
half, s, log
Defined Pair Symbols:
LOG, HALF
Compound Symbols:
c4, c2
(17) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
LOG(
s(
0)) →
c4(
S(
log(
0)),
LOG(
half(
s(
0))),
HALF(
s(
0)),
S(
0)) by
LOG(s(0)) → c4(LOG(half(s(0))))
(18) Obligation:
Complexity Dependency Tuples Problem
Rules:
half(0) → 0
half(s(0)) → 0
half(s(s(z0))) → s(half(z0))
s(log(0)) → s(0)
log(s(z0)) → s(log(half(s(z0))))
Tuples:
LOG(s(s(z0))) → c4(S(log(s(half(z0)))), LOG(half(s(s(z0)))), HALF(s(s(z0))), S(s(z0)))
HALF(s(s(s(s(s(s(z0))))))) → c2(S(s(s(half(z0)))), HALF(s(s(s(s(z0))))))
LOG(s(0)) → c4(LOG(half(s(0))))
S tuples:
LOG(s(s(z0))) → c4(S(log(s(half(z0)))), LOG(half(s(s(z0)))), HALF(s(s(z0))), S(s(z0)))
HALF(s(s(s(s(s(s(z0))))))) → c2(S(s(s(half(z0)))), HALF(s(s(s(s(z0))))))
LOG(s(0)) → c4(LOG(half(s(0))))
K tuples:none
Defined Rule Symbols:
half, s, log
Defined Pair Symbols:
LOG, HALF
Compound Symbols:
c4, c2, c4
(19) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
LOG(
s(
s(
z0))) →
c4(
S(
log(
s(
half(
z0)))),
LOG(
half(
s(
s(
z0)))),
HALF(
s(
s(
z0))),
S(
s(
z0))) by
LOG(s(s(x0))) → c4(S(s(log(half(s(half(x0)))))), LOG(half(s(s(x0)))), HALF(s(s(x0))), S(s(x0)))
LOG(s(s(0))) → c4(S(log(s(0))), LOG(half(s(s(0)))), HALF(s(s(0))), S(s(0)))
LOG(s(s(s(0)))) → c4(S(log(s(0))), LOG(half(s(s(s(0))))), HALF(s(s(s(0)))), S(s(s(0))))
LOG(s(s(s(s(z0))))) → c4(S(log(s(s(half(z0))))), LOG(half(s(s(s(s(z0)))))), HALF(s(s(s(s(z0))))), S(s(s(s(z0)))))
LOG(s(s(x0))) → c4(LOG(half(s(s(x0)))))
(20) Obligation:
Complexity Dependency Tuples Problem
Rules:
half(0) → 0
half(s(0)) → 0
half(s(s(z0))) → s(half(z0))
s(log(0)) → s(0)
log(s(z0)) → s(log(half(s(z0))))
Tuples:
HALF(s(s(s(s(s(s(z0))))))) → c2(S(s(s(half(z0)))), HALF(s(s(s(s(z0))))))
LOG(s(0)) → c4(LOG(half(s(0))))
LOG(s(s(x0))) → c4(S(s(log(half(s(half(x0)))))), LOG(half(s(s(x0)))), HALF(s(s(x0))), S(s(x0)))
LOG(s(s(0))) → c4(S(log(s(0))), LOG(half(s(s(0)))), HALF(s(s(0))), S(s(0)))
LOG(s(s(s(0)))) → c4(S(log(s(0))), LOG(half(s(s(s(0))))), HALF(s(s(s(0)))), S(s(s(0))))
LOG(s(s(s(s(z0))))) → c4(S(log(s(s(half(z0))))), LOG(half(s(s(s(s(z0)))))), HALF(s(s(s(s(z0))))), S(s(s(s(z0)))))
LOG(s(s(x0))) → c4(LOG(half(s(s(x0)))))
S tuples:
HALF(s(s(s(s(s(s(z0))))))) → c2(S(s(s(half(z0)))), HALF(s(s(s(s(z0))))))
LOG(s(0)) → c4(LOG(half(s(0))))
LOG(s(s(x0))) → c4(S(s(log(half(s(half(x0)))))), LOG(half(s(s(x0)))), HALF(s(s(x0))), S(s(x0)))
LOG(s(s(0))) → c4(S(log(s(0))), LOG(half(s(s(0)))), HALF(s(s(0))), S(s(0)))
LOG(s(s(s(0)))) → c4(S(log(s(0))), LOG(half(s(s(s(0))))), HALF(s(s(s(0)))), S(s(s(0))))
LOG(s(s(s(s(z0))))) → c4(S(log(s(s(half(z0))))), LOG(half(s(s(s(s(z0)))))), HALF(s(s(s(s(z0))))), S(s(s(s(z0)))))
LOG(s(s(x0))) → c4(LOG(half(s(s(x0)))))
K tuples:none
Defined Rule Symbols:
half, s, log
Defined Pair Symbols:
HALF, LOG
Compound Symbols:
c2, c4, c4
(21) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
LOG(
s(
0)) →
c4(
LOG(
half(
s(
0)))) by
LOG(s(0)) → c4(LOG(0))
LOG(s(0)) → c4
(22) Obligation:
Complexity Dependency Tuples Problem
Rules:
half(0) → 0
half(s(0)) → 0
half(s(s(z0))) → s(half(z0))
s(log(0)) → s(0)
log(s(z0)) → s(log(half(s(z0))))
Tuples:
HALF(s(s(s(s(s(s(z0))))))) → c2(S(s(s(half(z0)))), HALF(s(s(s(s(z0))))))
LOG(s(s(x0))) → c4(S(s(log(half(s(half(x0)))))), LOG(half(s(s(x0)))), HALF(s(s(x0))), S(s(x0)))
LOG(s(s(0))) → c4(S(log(s(0))), LOG(half(s(s(0)))), HALF(s(s(0))), S(s(0)))
LOG(s(s(s(0)))) → c4(S(log(s(0))), LOG(half(s(s(s(0))))), HALF(s(s(s(0)))), S(s(s(0))))
LOG(s(s(s(s(z0))))) → c4(S(log(s(s(half(z0))))), LOG(half(s(s(s(s(z0)))))), HALF(s(s(s(s(z0))))), S(s(s(s(z0)))))
LOG(s(s(x0))) → c4(LOG(half(s(s(x0)))))
LOG(s(0)) → c4(LOG(0))
LOG(s(0)) → c4
S tuples:
HALF(s(s(s(s(s(s(z0))))))) → c2(S(s(s(half(z0)))), HALF(s(s(s(s(z0))))))
LOG(s(s(x0))) → c4(S(s(log(half(s(half(x0)))))), LOG(half(s(s(x0)))), HALF(s(s(x0))), S(s(x0)))
LOG(s(s(0))) → c4(S(log(s(0))), LOG(half(s(s(0)))), HALF(s(s(0))), S(s(0)))
LOG(s(s(s(0)))) → c4(S(log(s(0))), LOG(half(s(s(s(0))))), HALF(s(s(s(0)))), S(s(s(0))))
LOG(s(s(s(s(z0))))) → c4(S(log(s(s(half(z0))))), LOG(half(s(s(s(s(z0)))))), HALF(s(s(s(s(z0))))), S(s(s(s(z0)))))
LOG(s(s(x0))) → c4(LOG(half(s(s(x0)))))
LOG(s(0)) → c4(LOG(0))
LOG(s(0)) → c4
K tuples:none
Defined Rule Symbols:
half, s, log
Defined Pair Symbols:
HALF, LOG
Compound Symbols:
c2, c4, c4, c4
(23) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 2 trailing nodes:
LOG(s(0)) → c4(LOG(0))
LOG(s(0)) → c4
(24) Obligation:
Complexity Dependency Tuples Problem
Rules:
half(0) → 0
half(s(0)) → 0
half(s(s(z0))) → s(half(z0))
s(log(0)) → s(0)
log(s(z0)) → s(log(half(s(z0))))
Tuples:
HALF(s(s(s(s(s(s(z0))))))) → c2(S(s(s(half(z0)))), HALF(s(s(s(s(z0))))))
LOG(s(s(x0))) → c4(S(s(log(half(s(half(x0)))))), LOG(half(s(s(x0)))), HALF(s(s(x0))), S(s(x0)))
LOG(s(s(0))) → c4(S(log(s(0))), LOG(half(s(s(0)))), HALF(s(s(0))), S(s(0)))
LOG(s(s(s(0)))) → c4(S(log(s(0))), LOG(half(s(s(s(0))))), HALF(s(s(s(0)))), S(s(s(0))))
LOG(s(s(s(s(z0))))) → c4(S(log(s(s(half(z0))))), LOG(half(s(s(s(s(z0)))))), HALF(s(s(s(s(z0))))), S(s(s(s(z0)))))
LOG(s(s(x0))) → c4(LOG(half(s(s(x0)))))
S tuples:
HALF(s(s(s(s(s(s(z0))))))) → c2(S(s(s(half(z0)))), HALF(s(s(s(s(z0))))))
LOG(s(s(x0))) → c4(S(s(log(half(s(half(x0)))))), LOG(half(s(s(x0)))), HALF(s(s(x0))), S(s(x0)))
LOG(s(s(0))) → c4(S(log(s(0))), LOG(half(s(s(0)))), HALF(s(s(0))), S(s(0)))
LOG(s(s(s(0)))) → c4(S(log(s(0))), LOG(half(s(s(s(0))))), HALF(s(s(s(0)))), S(s(s(0))))
LOG(s(s(s(s(z0))))) → c4(S(log(s(s(half(z0))))), LOG(half(s(s(s(s(z0)))))), HALF(s(s(s(s(z0))))), S(s(s(s(z0)))))
LOG(s(s(x0))) → c4(LOG(half(s(s(x0)))))
K tuples:none
Defined Rule Symbols:
half, s, log
Defined Pair Symbols:
HALF, LOG
Compound Symbols:
c2, c4, c4
(25) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)
Use forward instantiation to replace
HALF(
s(
s(
s(
s(
s(
s(
z0))))))) →
c2(
S(
s(
s(
half(
z0)))),
HALF(
s(
s(
s(
s(
z0)))))) by
HALF(s(s(s(s(s(s(s(s(y0))))))))) → c2(S(s(s(half(s(s(y0)))))), HALF(s(s(s(s(s(s(y0))))))))
(26) Obligation:
Complexity Dependency Tuples Problem
Rules:
half(0) → 0
half(s(0)) → 0
half(s(s(z0))) → s(half(z0))
s(log(0)) → s(0)
log(s(z0)) → s(log(half(s(z0))))
Tuples:
LOG(s(s(x0))) → c4(S(s(log(half(s(half(x0)))))), LOG(half(s(s(x0)))), HALF(s(s(x0))), S(s(x0)))
LOG(s(s(0))) → c4(S(log(s(0))), LOG(half(s(s(0)))), HALF(s(s(0))), S(s(0)))
LOG(s(s(s(0)))) → c4(S(log(s(0))), LOG(half(s(s(s(0))))), HALF(s(s(s(0)))), S(s(s(0))))
LOG(s(s(s(s(z0))))) → c4(S(log(s(s(half(z0))))), LOG(half(s(s(s(s(z0)))))), HALF(s(s(s(s(z0))))), S(s(s(s(z0)))))
LOG(s(s(x0))) → c4(LOG(half(s(s(x0)))))
HALF(s(s(s(s(s(s(s(s(y0))))))))) → c2(S(s(s(half(s(s(y0)))))), HALF(s(s(s(s(s(s(y0))))))))
S tuples:
LOG(s(s(x0))) → c4(S(s(log(half(s(half(x0)))))), LOG(half(s(s(x0)))), HALF(s(s(x0))), S(s(x0)))
LOG(s(s(0))) → c4(S(log(s(0))), LOG(half(s(s(0)))), HALF(s(s(0))), S(s(0)))
LOG(s(s(s(0)))) → c4(S(log(s(0))), LOG(half(s(s(s(0))))), HALF(s(s(s(0)))), S(s(s(0))))
LOG(s(s(s(s(z0))))) → c4(S(log(s(s(half(z0))))), LOG(half(s(s(s(s(z0)))))), HALF(s(s(s(s(z0))))), S(s(s(s(z0)))))
LOG(s(s(x0))) → c4(LOG(half(s(s(x0)))))
HALF(s(s(s(s(s(s(s(s(y0))))))))) → c2(S(s(s(half(s(s(y0)))))), HALF(s(s(s(s(s(s(y0))))))))
K tuples:none
Defined Rule Symbols:
half, s, log
Defined Pair Symbols:
LOG, HALF
Compound Symbols:
c4, c4, c2
(27) CpxTrsMatchBoundsProof (EQUIVALENT transformation)
A linear upper bound on the runtime complexity of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 1.
The certificate found is represented by the following graph.
Start state: 694
Accept states: [695, 696, 697]
Transitions:
694→695[half_1|0, 0|1]
694→696[s_1|0]
694→697[log_1|0]
694→694[0|0]
(28) BOUNDS(O(1), O(n^1))